$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it as}$,${\it bs}$:($T$ List), $x$:$T$. \\[0ex]($x$ $\in$ list{-}diff(${\it eq}$; ${\it as}$; ${\it bs}$)) $\Leftarrow\!\Rightarrow$ (($x$ $\in$ ${\it as}$) $\wedge$ ($\neg$($x$ $\in$ ${\it bs}$)))